$\forall$${\it es}$:ES, $A$:Type, ${\it Ia}$:AbsInterface($A$), $Q$:(E$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]Q{-}R{-}glued(${\it es}$; $A$; ($\lambda$$e$.${\it Ia}$($e$)); ${\it Ia}$; $Q$; ${\it Ia}$; $Q$)